In this paper we introduce a new type of nets with bounded types of distributed resources . Linear Logic to describe the behaviour of BR-nets is defined. It is based on Girard's Linear Logic but captures not only consumption of resources but their presence as well. Theorem of soundness and completeness of the proposed axiomatization is proved and the complexity of the provability problem is established for the general case and some particular ones.

Linear logic, introduced by Girard, is a refinement of classical logic with a natural, intrinsic accounting of resources. This accounting is made possible by removing the ‘structural’ rules of contraction and weakening, adding a modal operator and adding finer versions of the propositional connectives. Linear logic has fundamental logical interest and applications to computer science, particularly to Petri nets, concurrency, storage allocation, garbage collection and the control structure of logic programs. In addition, there is (...) a direct correspondence between polynomial-time computation and proof normalization in a bounded form of linear logic. In this paper we show that unlike most other propositional logics, full propositional linear logic is undecidable. Further, we prove that without the modal storage operator, which indicates unboundedness of resources, the decision problem becomes PSPACE-complete. We also establish membership in NP for the multiplicative fragment, NP-completeness for the multiplicative fragment extended with unrestricted weakening, and undecidability for fragments of noncommutative propositional linear logic. (shrink)

In this paper, we study temporal logic for finite linear structures and surjective bounded morphisms between them. We give a characterisation of such structures by modal formulas and show that every pair of linear structures with a bounded morphism between them can be uniquely characterised by a temporal formula up to an isomorphism. As the main result, we prove Kripke completeness of the logic with respect to the class of finite linear structures with (...) bounded morphisms between them. (shrink)

The depth-bounded approach seeks to provide realistic models of reasoners. Recognizing that most useful logics are idealizations in that they are either undecidable or likely to be intractable, the approach accounts for how they can be approximated in practice by resource-bounded agents. The approach has been applied to Classical Propositional Logic (CPL), yielding a hierarchy of tractable depth-bounded approximations to that logic, which in turn has been based on a KE/KI system. -/- This Thesis shows (...) that the approach can be naturally extended to useful nonclassical logics such as First-Degree Entailment (FDE), the Logic of Paradox (LP), Strong Kleene Logic (K3 ) and Intuitionistic Propositional Logic (IPL). To do this, we introduce a KE/KI-style system for each of those logics such that: is formulated via signed formulae, consist of linear operational rules and branching structural rule(s), can be used as a direct-proof and a refutation method, and is interesting independently of the approach in that it has an exponential speed-up on its tableau system counterpart. The latter given that we introduce a new class of examples which we prove to be hard for all tableau systems sharing the V/& rules with the classical one, but easy for their analogous KE-style systems. Then we focus on showing that each of our KE/KI-style systems naturally yields a hierarchy of tractable depth-bounded approximations to the respective logic, in terms of the maximum number of allowed nested applications of the branching rule(s). The rule(s) express(es) a generalized rule of bivalence, is (are) essentially cut rule(s) and govern(s) the manipulation of virtual information, which is information that an agent does not hold but she temporarily assumes as if she held it. Intuitively, the more virtual information needs to be invoked via the branching rule(s), the harder the inference is for the agent. So, the nested application the branching rule(s) provides a sensible measure of inferential depth. We also show that each hierarchy approximating FDE, LP, and K3 , admits of a 5-valued non-deterministic semantics; whereas, paving the way for a semantical characterization of the hierarchy approximating IPL, we provide a 3-valued non-deterministic semantics for the full logic that fixes the meaning of the connectives without appealing to “structural” conditions. -/- Moreover, we show a super-polynomial lower bound for the strongest possible version of clausal tableaux on the well-known class of “truly fat” expressions (which are easy for KE), settling a problem left open in the literature. Further, we investigate a hierarchy of tractable depth-bounded approximations to CPL based only on KE. Finally, we propose a refinement of the p-simulation relation which is adequate to establish positive results about the superiority of a system over another with respect to proof-search. (shrink)

In this paper, we consider multiplicative-additive fragments of affine propositional classical linear logic extended with n-contraction. To be specific, n-contraction (n 2) is a version of the contraction rule where (n+ 1) occurrences of a formula may be contracted to n occurrences. We show that expansions of the linear models for (n + 1)- valued ukasiewicz logic are models for the multiplicative-additive classical linear logic, its affine version and their extensions with n-contraction. We prove (...) the finite axiomatizability for the classes of finite models, as well as for the class of infinite linear models based on the set of rational numbers in the interval [0, 1]. The axiomatizations obtained in a Gentzen-style formulation are equivalent to finite and infinite-valued ukasiewicz logics. (shrink)

The theories Si1 and Ti1 are the analogues of Buss' relativized bounded arithmetic theories in the language where every term is bounded by a polynomial, and thus all definable functions grow linearly in length. For every i, a Σbi+1-formula TOPi, which expresses a form of the total ordering principle, is exhibited that is provable in Si+11 , but unprovable in Ti1. This is in contrast with the classical situation, where Si+12 is conservative over Ti2 w. r. t. Σbi+1-sentences. (...) The independence results are proved by translations into propositional logic, and using lower bounds for corresponding propositional proof systems. (shrink)

The set of unary functions of complexity classes defined by using bounded primitive recursion is inductively characterized by means of bounded iteration. Elementary unary functions, linear space computable unary functions and polynomial space computable unary functions are then inductively characterized using only composition and bounded iteration.

We introduce a three-tiered framework for modelling and reasoning about agents who (i) can use possibly complete reasoning systems without any restrictions but who nevertheless are (ii) bounded in the sense that they never reach infinitely many results and, finally, who (iii) perform their reasoning in time. This last aspect does not concern so much the time it takes for agents to actually carry out their reasoning, as the time which can bring about external changes in the agents’ states (...) such as arriving of new information or discarding previously available information due to bounds of the agent’s resources. These three aspects are treated with the maximal possible degree of independence from each other. The treatment of layer (iii) can be combined with arbitrary logic at level (ii) which, in turn, can be combined with arbitrary agent logic at level (i). At the level (iii), we discuss briefly the duality (or rather, complementarity) of system descriptions based on actions and transitions, on the one hand, and states and their changes, on the other. We settle for the latter and present a simple language, for describing state changes, which is parameterized by an arbitrary language for describing properties of the states. The language can be viewed as a simple fragment of step logic, admitting however various extensions by appropriate choices of the underlying logic. Alternatively, it can be seen as a very specific fragment of temporal logic (with a variant of ‘until’ or ‘chop’ operator), and is interpreted over dense linear time. The reasoning system presented here is sound, as well as strongly complete and decidable (provided that so is the parameter logic for reasoning about single states). We give the main idea of the completeness proof and suggest a wide range of possible applications, which is a simple consequence of the parametric character of both the language and the reasoning system. We address then in more detail the case of non-omniscient rational agents, (ii). Their models are syntactic structures (sets of available formulae) similar in spirit, though not in the technical formulation, to the models used in other syntax oriented approaches and in active logic. We give a new sound, complete and decidable system for reasoning about such agents. Finally, we illustrate its extensions with the internal reasoning of agents, (i), by equipping them with some example logics. (shrink)

A relation on a linearly ordered structure is called semi-bounded if it is definable in an expansion of the structure by bounded relations. We study ultimate behavior of semi-bounded relations in an ordered module M over an ordered commutative ring R such that M/rM is finite for all nonzero r $\epsilon$ R. We consider M as a structure in the language of ordered R-modules augmented by relation symbols for the submodules rM, and prove several quantifier elimination results (...) for semi-bounded relations and functions in M. We show that these quantifier elimination results essentially characterize the ordered modules M with finite indices of the submodules rM. It is proven that (1) any semi-bounded k-ary relation on M is equal, outside a finite union of k-strips, to a k-ary relation quantifier-free definable in M, (2) any semibounded function from $M^{k}$ to M is equal, outside a finite union of k-strips, to a piecewise linear function, and (3) any semi-bounded in M endomorphism of the additive group of M is of the form x $\mapsto \sigmax$ , for some $\mapsto \sigma$ from the field of fractions of R. (shrink)

In [U. Kohlenbach, Some logical metatheorems with applications in functional analysis, Trans. Amer. Math. Soc. 357 89–128], the second author obtained metatheorems for the extraction of effective bounds from classical, prima facie non-constructive proofs in functional analysis. These metatheorems for the first time cover general classes of structures like arbitrary metric, hyperbolic, CAT and normed linear spaces and guarantee the independence of the bounds from parameters ranging over metrically bounded spaces. Recently ]), the authors obtained generalizations of these (...) metatheorems which allow one to prove similar uniformities even for unbounded spaces as long as certain local boundedness conditions are satisfied. The use of classical logic imposes some severe restrictions on the formulas and proofs for which the extraction can be carried out. In this paper we consider similar metatheorems for semi-intuitionistic proofs, i.e. proofs in an intuitionistic setting enriched with certain non-constructive principles. Contrary to the classical case, there are practically no restrictions on the logical complexity of theorems for which bounds can be extracted. Again, our metatheorems guarantee very general uniformities, even in cases where the existence of uniform bounds is not obtainable by straightforward functional analytic means. Already in the purely intuitionistic case, where the existence of effective bounds is implicit, the metatheorems allow one to derive uniformities that may not be obvious at all from a given constructive proof. Finally, we illustrate our main metatheorem by an example from metric fixed point theory. (shrink)

We show that every model of IΔ0 has an end extension to a model of a theory where log-space computable function are formalizable. We also show the existence of an isomorphism between models of IΔ0 and models of linear arithmetic LA.

Agents need to be able to change their beliefs; in particular, they should be able to contract or remove a certain belief in order to restore consistency to their set of beliefs, and revise their beliefs by incorporating a new belief which may be inconsistent with their previous beliefs. An influential theory of belief change proposed by Alchourron, G¨ardenfors and Makinson (AGM) [1] describes postulates which a rational belief revision and contraction operations should satisfy. The AGM postulates have been perceived (...) as characterising idealised rational reasoners, and the corresponding belief change operations are considered unsuitable for implementable agents due to their high computational cost [3]. The main result of this paper is showing that an efficient (linear time) belief contraction operation nevertheless satisfies all but one of the AGM postulates for contraction. This contraction operation is defined for a realistic rule-based agent which can be seen as a reasoner in a very weak logic; although the agent’s beliefs are deductively closed with respect to this logic, checking consistency and tracing dependencies between beliefs is not computationally expensive. Finally, we give a non-standard definition of belief revision in terms of contraction for our agent. (shrink)

A proof of the (propositional) Craig interpolation theorem for cut-free sequent calculus yields that a sequent with a cut-free proof (or with a proof with cut-formulas of restricted form; in particular, with only analytic cuts) with k inferences has an interpolant whose circuit-size is at most k. We give a new proof of the interpolation theorem based on a communication complexity approach which allows a similar estimate for a larger class of proofs. We derive from it several corollaries: (1) Feasible (...) interpolation theorems for the following proof systems: (a) resolution (b) a subsystem of LK corresponding to the bounded arithmetic theory S 2 2 (α) (c) linear equational calculus (d) cutting planes. (2) New proofs of the exponential lower bounds (for new formulas) (a) for resolution ([15]) (b) for the cutting planes proof system with coefficients written in unary ([4]). (3) An alternative proof of the independence result of [43] concerning the provability of circuit-size lower bounds in the bounded arithmetic theory S 2 2 (α). In the other direction we show that a depth 2 subsystem of LK does not admit feasible monotone interpolation theorem (the so called Lyndon theorem), and that a feasible monotone interpolation theorem for the depth 1 subsystem of LK would yield new exponential lower bounds for resolution proofs of the weak pigeonhole principle. (shrink)

We investigate a SAT-based bounded model checking method for EMTLK that is interpreted over timed models generated by timed interpreted systems. In particular, we translate the existential model checking problem for EMTLK to the existential model checking problem for a variant of linear temporal logic, and we provide a SAT-based BMC technique for HLTLK. We evaluated the performance of our BMC by means of a variant of a timed generic pipeline paradigm scenario and a timed train controller (...) system. (shrink)

We show that the bounded arithmetic theory V0 does not prove that the polynomial time hierarchy collapses to the linear time hierarchy . The result follows from a lower bound for bounded depth circuits computing prefix parity, where the circuits are allowed some auxiliary input; we derive this from a theorem of Ajtai.

After the seminal work of Kraus, Lehmann and Magidor (formally known as the KLM approach) on conditionals and preferential models, many aspects of defeasibility in more complex formalisms have been studied in recent years. Examples of these aspects are the notion of typicality in description logic and defeasible necessity in modal logic. We discuss a new aspect of defeasibility that can be expressed in the case of temporal logic, which is the normality in an execution. In this (...) contribution, we take Linear Temporal Logic (LTL) as case study for this defeasible aspect. LTL has found extensive applications in Computer Science and Artificial Intelligence, notably as a formal framework for representing and verifying computer systems that vary over time. However, some systems may presents exceptions at some innocuous time points where they can be tolerated, or conversely, exceptions at other crucial time points where they need to be addressed. In order to ensure the reliability of such systems, we study a preferential extension of LTL, called defeasible linear temporal logic (LTL ~ ). In the first part of this paper, we show how semantics of KLM's preferential models can be integrated with LTL. We also discuss the addition of non-monotonic temporal operators as a way to formalise defeasible properties of these systems. The second part of this paper is a study of the satisfiability problem of LTL ~ sentences. Based on Sistla and Clarke's work on the complexity of the classical LTL language, we show the bounded-model property of two fragments of LTL ~ language. Moreover, we provide a procedure to check the satisfiability of sentences in both of these fragments. (shrink)

There are several areas in applied logic where deletion from databases is involved in one way or another:Belief contraction Triggers of the form ‘If condition then remove A’, which are extensively used in database management systemsResource considerations as in relevance and linear logics, where addition or removal of resource can affect provabilityFree logic and the like, where existence and non-existence of individuals affects quantification.All of these areas have certain logical difficulties relating to the removal of elements. This (...) paper points out the difficulties and offers a comprehensive logical model. (shrink)

FDE, LP and K3 are closely related to each other and admit of an intuitive informational interpretation. However, all these logics are co-NP complete, and so idealized models of how an agent can think. We address this issue by shifting to signed formulae, where the signs express imprecise values associated with two bipartitions of the corresponding set of standard values. We present proof systems whose operational rules are all linear and have only two structural branching rules that express a (...) generalized Principle of Bivalence. Each of these systems leads to defining an infinite hierarchy of tractable approximations to the respective logic, in terms of the maximum number of allowed nested applications of the two branching rules. Further, each resulting hierarchy admits of an intuitive 5-valued non-deterministic semantics. (shrink)

Theories of classification distinguish classes with some good structure theorem from those for which none is possible. Some classes (dense linear orders, for instance) are non-classifiable in general, but are classifiable when we consider only countable members. This paper explores such a notion for classes of computable structures by working out a sequence of examples. We follow recent work by Goncharov and Knight in using the degree of the isomorphism problem for a class to distinguish classifiable classes from non-classifiable. (...) In this paper, we calculate the degree of the isomorphism problem for Abelian p-groups of bounded Ulm length. The result is a sequence of classes whose isomorphism problems are cofinal in the hyperarithmetical hierarchy. In the process, new back-and-forth relations on such groups are calculated. (shrink)

In this note we show: Let R = 〈R, <, +, 0, …〉 be a semi-bounded o-minimal expansion of an ordered group, and G a group definable in R of linear dimension m . Then G is a definable extension of a bounded definable group B by 〈Rm, +〉.

We show that both the $n$-density and the bounded $n$-width of Kripke frames can be modally defined not only with natural and well-known Sahlqvist formulae containing a linear number of different propositional variables but also with formulae of polynomial length with a logarithmic number of different propositional variables and then we prove that this exponential decrease in the number of variables leads us outside the class of Sahlqvist formulae.

LetB be the set of bounded observables on a quantum logic. A mapJ: B →R is called an expectation functional ifJ is normalized, positive, continuous, and compatibly linear. Two questions are considered. IsJ linear, and isJ an expectation relative to some state? It is shown that the answers are affirmative for hidden variable logics and most Hilbert space logics. An example is given which shows thatJ can be nonlinear on an arbitrary quantum logic.

Temporal epistemic logics are known, from results of Halpern and Vardi, to have a wide range of complexities of the satisfiability problem: from PSPACE, through non-elementary, to highly undecidable. These complexities depend on the choice of some key parameters specifying, inter alia, possible interactions between time and knowledge, such as synchrony and agents' abilities for learning and recall. In this work we develop practically implementable tableau-based decision procedures for deciding satisfiability in single-agent synchronous temporal-epistemic logics with interactions between time and (...) knowledge. We discuss some complications that occur, even in the single-agent case, when interactions between time and knowledge are assumed and show how the method of incremental tableaux can be adapted to work in EXPSPACE, respectively 2EXPTIME, for these logics, thereby also matching the upper bounds obtained for them by Halpern and Vardi. (shrink)

We develop a timeout extension of propositional linear temporal logic to specify timing properties of timeout-based models of real-time systems. A timeout is used to model the execution of an action marking the end of a delay. With a view to expressing such timeout constraints, ToLTL uses a dynamic variable to abstract the timeout behaviour in addition to a variable which captures the global clock and some static timing variables which record time instances when discrete events occur. We (...) propose a corresponding timeout tableau for satisfiability checking of the ToLTL formulas. Further we prove that the validity checking for such an extended logic remains PSPACE-complete. Under discrete time semantics, with bounded timeout increments, the model-checking problem which verifies if a ToLTL-formula holds in a timeout Kripke structure is also shown to be PSPACE complete. We further prove that ToLTL, when interpreted over discrete time, can be embedded in the monadic second-order logic with.. (shrink)

We carry out a systematic investigation of the definability of linear order on classes of finite rigid structures. We obtain upper and lower bounds for the expressibility of linear order in various logics that have been studied extensively in finite model theory, such as least fixpoint logic LFP, partial fixpoint logic PFP, infinitary logic Lω∞ω with a finite number of variables, as well as the closures of these logics under implicit definitions. Moreover, we show that (...) the upper and lower bounds established here cannot be made substantially tighter, unless outstanding conjectures in complexity theory are resolved at the same time. (shrink)

Substructural fuzzy logics are substructural logics that are complete with respect to algebras whose lattice reduct is the real unit interval [0.1]. In this paper, we introduce Uninorm logic UL as Multiplicative additive intuitionistic linear logic MAILL extended with the prelinearity axiom ((A → B) ∧ t) ∨ ((B → A) ∧ t). Axiomatic extensions of UL include known fuzzy logics such as Monoidal t-norm logic MTL and Gödel logic G, and new weakening-free logics. Algebraic (...) semantics for these logics are provided by subvarieties of (representable) pointed bounded commutative residuated lattices. Gentzen systems admitting cut-elimination are given in the framework of hypersequents. Completeness with respect to algebras with lattice reduct [0, 1] is established for UL and several extensions using a two-part strategy. First, completeness is proved for the logic extended with Takeuti and Titani's density rule. A syntactic elimination of the rule is then given using a hypersequent calculus. As an algebraic corollary, it follows that certain varieties of residuated lattices are generated by their members with lattice reduct [0, 1]. (shrink)

In our former works, for a given concept of reduction, we study the following hypothesis: “For a random oracle A, with probability one, the degree of the one-query tautologies with respect to A is strictly higher than the degree of A.” In our former works (Suzuki in Kobe J. Math. 15, 91–102, 1998; in Inf. Comput. 176, 66–87, 2002; in Arch. Math. Logic 44, 751–762), the following three results are shown: The hypothesis for p-T (polynomial-time Turing) reduction is equivalent (...) to the assertion that the probabilistic complexity class R is not equal to NP; The hypothesis for p-tt (polynomial-time truth-table) reduction implies that P is not NP; The hypothesis holds for each of the following: disjunctive reduction, conjunctive reduction, and p-btt (polynomial-time bounded-truth-table) reduction. In this paper, we show the following three results: (1) Let c be a positive real number. We consider a concept of truth-table reduction whose norm is at most c times size of input, where for a relativized propositional formula F, the size of F denotes the total number of occurrences of propositional variables, constants and propositional connectives. Then, our main result is that the hypothesis holds for such tt-reduction, provided that c is small enough. How small c can we take so that the above holds? It depends on our syntactic convention on one-query tautologies. In our setting, the statement holds for all c < 1. (2) The hypothesis holds for monotone truth-table reduction (also called positive reduction). (3) Dowd (in Inf. Comput. 96, 65–76, 1992) shows a polynomial upper bound for the minimum sizes of forcing conditions associated with a random oracle. We apply the above result (1), and get a linear lower bound for the sizes. (shrink)

We introduce new proof systems for propositional logic, simple deduction Frege systems, general deduction Frege systems, and nested deduction Frege systems, which augment Frege systems with variants of the deduction rule. We give upper bounds on the lengths of proofs in Frege proof systems compared to lengths in these new systems. As applications we give near-linear simulations of the propositional Gentzen sequent calculus and the natural deduction calculus by Frege proofs. The length of a proof is the number (...) of lines in the proof. A general deduction Frege proof system provides at most quadratic speedup over Frege proof systems. A nested deduction Frege proof system provides at most a nearly linear speedup over Frege system where by "nearly linear" is meant the ratio of proof lengths is O) where α is the inverse Ackermann function. A nested deduction Frege system can linearly simulate the propositional sequent calculus, the tree-like general deduction Frege calculus, and the natural deduction calculus. Hence a Frege proof system can simulate all those proof systems with proof lengths bounded by O). Also we show that a Frege proof of n lines can be transformed into a tree-like Frege proof of O lines and of height O. As a corollary of this fact we can prove that natural deduction and sequent calculus tree-like systems simulate Frege systems with proof lengths bounded by O. (shrink)

A full separation theorem for the derivable rules of intuitionistic linear logic without bounds, 0 and exponentials is proved. Several structural consequences of this theorem for subreducts of (commutative) residuated lattices are obtained. The theorem is then extended to the logic LR+ and its proof is extended to obtain the finite embeddability property for the class of square increasing residuated lattices.

In this article we investigate the complexity of isomorphisms between scattered linear orders of constructive ranks. We give the general upper bound and prove that this bound is sharp. Also, we construct examples showing that the categoricity level of a given scattered linear order can be an arbitrary ordinal from 3 to the upper bound, except for the case when the ordinal is the successor of a limit ordinal. The existence question of the scattered linear orders whose (...) categoricity level equals the successor of a limit ordinal is still open. (shrink)

In this article we investigate the complexity of isomorphisms between scattered linear orders of constructive ranks. We give the general upper bound and prove that this bound is sharp. Also, we construct examples showing that the categoricity level of a given scattered linear order can be an arbitrary ordinal from 3 to the upper bound, except for the case when the ordinal is the successor of a limit ordinal. The existence question of the scattered linear orders whose (...) categoricity level equals the successor of a limit ordinal is still open. (shrink)

We investigate the theories of linear algebra, which were originally defined to study the question of whether commutativity of matrix inverses has polysize Frege proofs. We give sentences separating quantified versions of these theories, and define a fragment in which we can interpret a weak theory V 1 of bounded arithmetic and carry out polynomial time reasoning about matrices - for example, we can formalize the Gaussian elimination algorithm. We show that, even if we restrict our language, proves (...) the commutativity of inverses. (shrink)

A first-order temporal non-commutative logic TN[l], which has no structural rules and has some l-bounded linear-time temporal operators, is introduced as a Gentzen-type sequent calculus. The logic TN[l] allows us to provide not only time-dependent, resource-sensitive, ordered, but also hierarchical reasoning. Decidability, cut-elimination and completeness (w.r.t. phase semantics) theorems are shown for TN[l]. An advantage of TN[l] is its decidability, because the standard first-order linear-time temporal logic is undecidable. A correspondence theorem between TN[l] and (...) a resource indexed non-commutative logic RN[l] is also shown. This theorem is intended to state that “time” is regarded as a “resource”. (shrink)

We develop and study the complexity of propositional proof systems of varying strength extending resolution by allowing it to operate with disjunctions of linear equations instead of clauses. We demonstrate polynomial-size refutations for hard tautologies like the pigeonhole principle, Tseitin graph tautologies and the clique-coloring tautologies in these proof systems. Using interpolation we establish an exponential-size lower bound on refutations in a certain, considerably strong, fragment of resolution over linear equations, as well as a general polynomial upper bound (...) on interpolants in this fragment.We then apply these results to extend and improve previous results on multilinear proofs , as studied in [Ran Raz, Iddo Tzameret, The strength of multilinear proofs. Comput. Complexity ]. Specifically, we show the following:• Proofs operating with depth-3 multilinear formulas polynomially simulate a certain, considerably strong, fragment of resolution over linear equations.• Proofs operating with depth-3 multilinear formulas admit polynomial-size refutations of the pigeonhole principle and Tseitin graph tautologies. The former improve over a previous result that established small multilinear proofs only for the functional pigeonhole principle. The latter are different from previous proofs, and apply to multilinear proofs of Tseitin mod p graph tautologies over any field of characteristic 0. We conclude by connecting resolution over linear equations with extensions of the cutting planes proof system. (shrink)

Infinitary action logic can be naturally expanded by adding exponential and subexponential modalities from linear logic. In this article we shall develop infinitary action logic with a subexponential that allows multiplexing (instead of contraction). Both non-commutative and commutative versions of this logic will be considered, presented as infinitary sequent calculi. We shall prove cut admissibility for these calculi, and estimate the complexity of the corresponding derivability problems: in both cases it will turn out to be (...) between complete first-order arithmetic and the $\omega ^\omega$ level of the hyperarithmetical hierarchy. Here the complexity upper bound is much lower than that for the system with a subexponential that allows contraction. The complexity lower bound in turn is much higher than that for infinitary action logic. (shrink)

This article systematically investigates so-called “truth variants” of several functional interpretations. We start by showing a close relation between two variants of modified realizability, namely modified realizability with truth and q-modified realizability. Both variants are shown tobe derived from a single “functional interpretation with truth” of intuitionistic linear logic. This analysis suggests that several functional interpretations have truth and q-variants. These variants, however, require a more involved modification than the ones previously considered. Following this lead we present truth (...) and q-variants of the Diller-Nahm interpretation, the bounded modified realizability and the bounded functional interpretation. (shrink)

The relationship between Lexical-Functional Grammar (LFG) functional structures (f-structures) for sentences and their semanticinterpretations can be formalized in linear logic in a way thatcorrectly explains the observed interactions between quantifier scopeambiguity, bound anaphora and intensionality.Our linear-logic formalization of the compositional properties ofquantifying expressions in natural language obviates the need forspecial mechanisms, such as Cooper storage, in representing thescoping possibilities of quantifying expressions. Instead, thesemantic contribution of a quantifier is recorded as a linear-logicformula whose use in (...) a proof will establish the scope of thequantifier. Different proofs can lead to different scopes. In eachcomplete proof, the properties of linear logic ensure thatquantifiers are properly scoped. (shrink)

We calculate the complexity of Scott sentences of scattered linear orders. Given a countable scattered linear order L of Hausdorff rank $\alpha $ we show that it has a ${d\text {-}\Sigma _{2\alpha +1}}$ Scott sentence. It follows from results of Ash [2] that for every countable $\alpha $ there is a linear order whose optimal Scott sentence has this complexity. Therefore, our bounds are tight. We furthermore show that every Hausdorff rank 1 linear order has an (...) optimal ${\Pi ^{\mathrm {c}}_{3}}$ or ${d\text {-}\Sigma ^{\mathrm {c}}_{3}}$ Scott sentence and give a characterization of those linear orders of rank $1$ with ${\Pi ^{\mathrm {c}}_{3}}$ optimal Scott sentences. At last we show that for all countable $\alpha $ the class of Hausdorff rank $\alpha $ linear orders is $\boldsymbol {\Sigma }_{2\alpha +2}$ complete and obtain analogous results for index sets of computable linear orders. (shrink)

We consider the Lambek calculus, or noncommutative multiplicative intuitionistic linear logic, extended with iteration, or Kleene star, axiomatised by means of an$\omega $-rule, and prove that the derivability problem in this calculus is$\Pi _1^0$-hard. This solves a problem left open by Buszkowski (2007), who obtained the same complexity bound for infinitary action logic, which additionally includes additive conjunction and disjunction. As a by-product, we prove that any context-free language without the empty word can be generated by a (...) Lambek grammar with unique type assignment, without Lambek’s nonemptiness restriction imposed (cf. Safiullin, 2007). (shrink)

Let F be a signature and R a strictly orthogonal rewrite system on ground terms of F . We give an effective proof of a bounding condition for R , based on a detailed analysis of how terms are transformed during the rewrite process, which allows us to give recursive bounds on the derivation lengths of terms. We give a syntactic characterisation of the Grzegorczyk hierarchy and a rewriting schema for calculating its functions. As a consequence of this, using results (...) of Elias Tahhan–Bittar, it can be shown that, for n⩾3 , the derivation length functions for functions in Grzegorczyk class E n belong to Grzegorczyk class E n+1 . We also give recursive bounds for the derivation lengths of functions defined by parameter recursion. (shrink)

We investigate structures recognizable by finite state automata with an input tape of length a limit ordinal. At limits, the set of states which appear unboundedly often before the limit are mapped to a limit state. We describe a method for proving non-automaticity and apply this to determine the optimal bounds for the ranks of linear orders recognized by such automata.

In this paper I will communicate some new consequences of the Proper Forcing Axiom. First, the Bounded Proper Forcing Axiom implies that there is a well ordering of R which is Σ 1 -definable in (H(ω 2 ), ∈). Second, the Proper Forcing Axiom implies that the class of uncountable linear orders has a five element basis. The elements are X, ω 1 , ω 1 * , C, C * where X is any suborder of the reals (...) of size ω 1 and C is any Countryman line. Third, the Proper Forcing Axiom implies the Singular Cardinals Hypothesis at κ unless stationary subsets of S κ + ω reflect. The techniques are expected to be applicable to other open problems concerning the theory of H(ω 2 ). (shrink)

The provability logic of a theory $T$ is the set of modal formulas, which under any arithmetical realization are provable in $T$. We slightly modify this notion by requiring the arithmetical realizations to come from a specified set $\Gamma$. We make an analogous modification for interpretability logics. We first study provability logics with restricted realizations and show that for various natural candidates of $T$ and restriction set $\Gamma$, the result is the logic of linear frames. However, for (...) the theory Primitive Recursive Arithmetic (PRA), we define a fragment that gives rise to a more interesting provability logic by capitalizing on the well-studied relationship between PRA and I$\Sigma_1$. We then study interpretability logics, obtaining upper bounds for IL(PRA), whose characterization remains a major open question in interpretability logic. Again this upper bound is closely related to linear frames. The technique is also applied to yield the nontrivial result that IL(PRA) $\subset$ ILM. (shrink)